es:event_system{i:l}, e:es-E(es). es_state_when(es; e)  es_state(es; loc(e)) 

latex

Definitions

t  T, x:A. B(x), es-pred!(es; e; e'), SWellFounded(R(x;y)), P  Q, loc(e), <a, b>, Id, s = t, es_state(es; i), x:A  B(x), when-after(e;info;pred?;init;Trans;val;time), EState(T), Type, x:AB(x), x. t(x), t.1, b, pred!(e;e'), first(e), A, loc(e), IdLnk, es-kind(es; e), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t)), subtype(S; T), suptype(S; T), Knd, es_state_when(es; e), event_system{i:l}, es_time(es), es_val(es), es-Trans(es), es_init(es), es_info(es), es-pred?(es), es-M(es), es-V(es), es-T(es), f(a), x.A(x), es-E(es)

Lemmas

event system wf, when-after wf, es info wf, es init wf, es-Trans wf, Knd wf, es val wf, kindcase wf, es-kind wf, es-V wf, es-M wf, Id wf, IdLnk wf, es time wf, not wf, assert wf, first wf, es-pred? wf, es-E wf, pi1 wf, EState wf, es state wf, es-T wf, es-loc wf, es-loc-pred, es-pred!-wellfounded